#pragma once

#include <vector>
#include <list>
#include "constants.h"
#include "clause.h"
#include "decision.h"
#include "istrategy.h"
#include "problem_variable.h"
#include "conflict.h"
#include <fstream>

namespace solver
{
	class problem_solver
	{
	public:
		std::function<void(const char *message)> progress_func;
		int index;
		std::string problem_name;
		std::vector<problem_variable> variables;
		std::vector<pdecision> decisions;
		std::vector<pproduction> productions;
		decision_string_collection production_index;
		std::string comments;
		decision_string solution;
		int resolution_count;

		bool trace_enabled;
		int trace_index;
		bool trace_started;
		int pass_count;

		problem_solver()
		{
			clear();
		}

		~problem_solver()
		{
			clear();
		}

		void clear()
		{
			pass_count = 0;
			srand(0);
			index = 0;
			solution.clear();
			problem_name.clear();
			variables.clear();
			comments.clear();
			for (int i = 0; i < decisions.size(); i++)
			{
				delete decisions[i];
				decisions[i] = nullptr;
			}
			decisions.clear();
			trace_enabled = false;
			trace_index = 0;
			trace_started = false;
		}

		class guess_literal_result
		{
		public:
			bool success;
			bool complete;
			bool conflict;
			literal guess;
			decision *dec;

			guess_literal_result() : success(false), complete(false), conflict(false), dec(nullptr)
			{

			}
		};

		class apply_literal_result
		{
		public:
			bool success;
			bool unsolveable;
			bool conflicted_guess;
			std::string failreason;

			apply_literal_result() : success(false), unsolveable(false), conflicted_guess(false)
			{

			}
		};

		class step_result 
		{
		public:
			bool finished;
			bool solved;
			bool unsolveable;
			std::string reason;

			step_result() : finished(false), solved(false), unsolveable(false)
			{

			}

			apply_literal_result apply_result;
			guess_literal_result guess_result;
		};

		step_result last_step_result;

		step_result step(solver::istrategy& solver_strategy)
		{
			pass_count++;

			step_result result;
			
			result.guess_result = guess_literal();

			if (result.guess_result.complete)
			{
				result.finished = true;
				if (result.guess_result.conflict)
				{
					result.unsolveable = true;
					result.reason = "Internal error conflict with clause "; 
					result.reason += to_string(result.guess_result.dec);
				}
				else 
				{
					result.solved = true;
					result.reason = "Guess string is the solution";
				}
				last_step_result = result;

				return result;
			}
			else 
			{
				result.apply_result = apply_literal(result.guess_result.guess);
				if (result.apply_result.conflicted_guess)
				{
					result.unsolveable = true;
					result.reason = result.apply_result.failreason;
				}
				else if (result.apply_result.unsolveable)
				{
					result.unsolveable = true;
					result.reason = result.apply_result.failreason;
				}
			}
			last_step_result = result;
			apply_solution(solver_strategy);
			return result;
		}

		bool solve(solver::istrategy& solver_strategy)
		{
			step_result result;
			do
			{
				result = step(solver_strategy);
			} while (!result.finished);

			if (!result.solved)
			{
				solution.clear();
			}
			return result.solved;
		}

		std::string to_string(solver::pdecision dec)
		{
			std::string text;

			text = "(";
			bool written = false;
			int ds = dec->literals.size();
			for (int i = 0; i < ds; i++)
			{
				auto& vs = dec->literals[i];

				if (written) {
					text += " | ";
				}
				auto& v = variables[vs.ref];

				if (vs.val == 0) {
					text += "!";
					text += std::to_string(v.name);
				}
				else
				{
					text += std::to_string(v.name);
				}
				written = true;
			}
			text += ")";

			return text;
		}

		std::string to_string(solver::decision_string& dstr, const char *delimiter = nullptr)
		{
			std::string x = "";
			if (dstr.is_c_str) {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}
					std::string temp(1, (char)variables[dcdest.ref].name);
					x += temp;
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			else {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}

					x += std::to_string(variables[dcdest.ref].name);
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			return x;

		}


	private:

		void apply_solution(solver::istrategy& solver_strategy)
		{
			int vc = variables.size();
			int ds = decisions.size();
			int i;
			int t;

			for (i = 0; i < ds; i++)
			{
				auto dec = decisions[i];
				dec->selected_literal = -1;
			}

			for (i = 0; i < vc; i++)
			{
				auto& v = variables[i];
				v.check_valid = true;
				v.value = -1;
			}
			
			auto dcdestn = solution.first();
			while (dcdestn != nullptr)
			{
				auto& ch = dcdestn->value;

				auto& v = variables[ch.ref];
				t = ch.val;

				if (v.check_valid && (v.value == -1 || v.value == t))
				{
					v.value = t;
				}
				else
				{
					v.check_valid = false;
				}

				int ds = decisions.size();
				for (int j = 0; j < ds; j++) 
				{
					auto dec = decisions[j];
					for (int i = 0; i < dec->literals.size(); i++)
					{
						if (ch == dec->literals[i]) 
						{
							dec->selected_literal = i;
							break;
						}
					}
				}
				dcdestn = solution.next(dcdestn);
			}
		}


		// literal get_next_literal() returns the next literal from the next unsolved clause as a guess.
		// if the returned result is -1, then the problem is solved.
		// todo, accelerate
		guess_literal_result guess_literal()
		{
			guess_literal_result result;

			int nd = decisions.size();
			for (int i = 0; i < nd; i++)
			{
				decision *dec = decisions[i];
				int nds = dec->literals.size();
				bool found = false;
				for (int j = 0; j < nds && !found; j++)
				{
					if (solution.exists_exact(dec->literals[j])) 
					{
						found = true;
					}
				}
				if (!found)
				{
					result.dec = dec;
					for (int j = 0; j < nds; j++)
					{
						result.guess = dec->literals[j];
						if (!solution.exists(result.guess)) 
						{
							result.success = true;
							return result;
						}
					}
					result.conflict = true;
					result.complete = true;
					return result;
				}
			}

			result.complete = true;
			return result;
		}

		pproduction produces_conflict(decision_string ds, multiconflict_iterator& conflicts, bool test)
		{
			bool implying = false;
			int psz = productions.size();

			do
			{
				std::list<literal_node *> found_strings;
				production_index.find_strings(ds, found_strings);

				for (auto& nd : found_strings)
				{
					auto& prd = productions[nd->string_id];
					if (prd->product.ref > -1)
					{
						bool res = ds.add(prd->product);
						if (!res) 
						{
							if (!test) {
								std::string conf = "->";
								conf += to_string(prd->match, " ");
								write_console(conf);
								conf += "\n";
								OutputDebugString(conf.c_str());
								conflicts.add(prd);
							}
							return prd;
						}
					}
					else
					{
						if (!test) {
							std::string conf = "->";
							conf += to_string(prd->match, " ");
							write_console(conf);
							conf += "\n";
							OutputDebugString(conf.c_str());
							conflicts.add(prd);
						}
						return prd;
					}
				}
				implying = productions.size() > psz;
				psz = productions.size();
			} while (implying);

			return nullptr;
		}

		class resolve_conflict_result {
		public:

			bool resolved;
			std::string reason;

		};

		resolve_conflict_result resolve_conflict(multiconflict_iterator& conflicts)
		{
			resolve_conflict_result result;

			write_console("Resolving conflicts");

			bool found_conflicts = true;

			result.resolved = true;
			result.reason = "Ok";

			int count = 0;
			pproduction prodstep = nullptr;
			decision_string prodstepsolution;

			while (conflicts.size() < 20)
			{

				bool found_solution = true;
				found_solution = conflicts.get_first(solution);
				while (found_solution)
				{
					decision_string temps = solution;
					std::string temp = to_string(conflicts.last_result, " ");
					temp += " - solving";
					write_console(temp);
					auto prod = produces_conflict(temps, conflicts, true);
					if (!prod)
					{
						write_console("resolved");
						found_conflicts = false;
						result.resolved = true;
						return result;
					}
					if (!prodstep)
					{
						prodstep = prod;
						prodstepsolution = temps;
					}
					found_solution = conflicts.get_next(solution);
				}

				if (prodstep)
				{
					write_console("expand");
					solution = prodstepsolution;
					conflicts.add(prodstep);
					prodstep = nullptr;
				}
			}

			result.reason = "too hard for us, so we bailed.";
			result.resolved = false;
			return result;

		}

		void write_console(const char * src)
		{
			std::string temp;
			temp = src;
			write_console(temp);
		}

		void write_console(decision_string& src)
		{
			std::string temp;
			temp = to_string(src);
			write_console(temp);
		}

		void write_console(std::string& src)
		{
			OutputDebugString(src.c_str());
			OutputDebugString("\n");
			if (progress_func) {
				progress_func(src.c_str());
			}
		}

		apply_literal_result apply_literal(literal guess)
		{
			apply_literal_result result;
			// clear conflicts
			bool initial_guess_bad = false;

			bool decent_guess = solution.add(guess);
			if (!decent_guess)
			{
				// this should never happen
				result.conflicted_guess = true;
				return result;
			}

			bool found_conflicts = false;
			bool adding_implications = false;

			multiconflict_iterator conflicts;

			write_console("Implications");

			do 
			{
				std::list<literal_node *> found_strings;
				production_index.find_strings(solution, found_strings);
				int current_solution_size = solution.size();

				for (auto& nd : found_strings)
				{
					auto& prd = productions[nd->string_id];
					if (prd->product.ref > -1)
					{
						bool added = solution.add(prd->product);
						if (!added) 
						{
							found_conflicts = true;
							write_console(prd->match);
							conflicts.add(prd);
						}
					}
					else
					{
						found_conflicts = true;
						write_console(prd->match);
						conflicts.add(prd);
					}
				}

				adding_implications = solution.size() > current_solution_size;
			} while (adding_implications);

			auto conf = produces_conflict(solution, conflicts, false);
			if (conf != nullptr)
			{
				found_conflicts = true;
			}

			if (found_conflicts) 
			{
				auto resolve_result = resolve_conflict(conflicts);
				result.unsolveable = !resolve_result.resolved;
				result.failreason = resolve_result.reason;
				result.success = resolve_result.resolved;
				result.conflicted_guess = false;
			}
			else 
			{
				result.conflicted_guess = false;
				result.success = true;
			}

			return result;

		}

	};
}
